package tr.edu.ege.kipler.satisfiability.completion.rules.dl;

import java.util.Iterator;

import tr.edu.ege.kipler.satisfiability.ReasonerException;
import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.blocking.BlockingStrategy;
import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.ConceptCategory;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.RBox;
import tr.edu.ege.kipler.satisfiability.container.WcsData;
import tr.edu.ege.kipler.syntax.Role;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.ObjectRoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.RoleAssertion.Type;
import tr.edu.ege.kipler.syntax.concept.Concept;
import tr.edu.ege.kipler.syntax.concept.RoleQuantification;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class TransitivityRule extends ABoxRule {
	private ABox aBox;

	private boolean applied;

	private BlockingStrategy blocking;

	public TransitivityRule(BlockingStrategy blocking) {
		setBlocking(blocking);
	}

	public BlockingStrategy getBlocking() {
		return blocking;
	}

	public void setBlocking(BlockingStrategy blocking) {
		this.blocking = blocking;
	}

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		aBox = getWorld().getABox();
		RBox rBox = getWorld().getRBox();
		if (!getBlocking().isIndirectlyBlocked(aBox, getIndividual().getName())) {
			for (Iterator<Concept> i = getIndividual().conceptIterator(
					ConceptCategory.ALL); i.hasNext();) {
				Concept concept = i.next();
				RoleQuantification rq = (RoleQuantification) concept;
				for (Role subRole : rBox.getSubRoles(rq.getRole())) {
					if (rBox.contains(new RoleAssertion(Type.TRANSITIVE,
							subRole))) {
						addValueRestrictionToNeighbors(subRole, rq);
					}
				}
			}
		}
	}

	private void addValueRestrictionToNeighbors(Role role,
			RoleQuantification restriction) throws UnsatisfiableException {
		Iterator<ObjectRoleAssertion> raIter = aBox.neighborIterator(role,
				getIndividual());
		while (raIter.hasNext()) {
			ObjectRoleAssertion ra = raIter.next().normalize(
					getIndividual().getName());
			Individual filler = aBox.getIndividual(ra.getFiller());
			ConceptAssertion newConAssert = new ConceptAssertion(restriction,
					filler.getName());
			if (!aBox.contains(newConAssert)) {
				WcsData wcsData = getWcs().getData();
				wcsData.getLogger().info(
						"WCS " + getWcs().getId()
								+ " Transitivity rule: Adding " + newConAssert);
				wcsData.getDependencyManager().move(
						newConAssert,
						new ConceptAssertion(restriction, getIndividual()
								.getName()));
				wcsData.getDependencyManager().move(newConAssert, ra);
				aBox.add(newConAssert);
				applied = true;
			}
		}
	}

	@Override
	public boolean isApplied() {
		return applied;
	}

}
